Problema del tablero de ajedrez mutilado

Problema del tablero de ajedrez mutilado

El problema del tablero de ajedrez mutilado es un rompecabezas de enlosado propuesto por el filósofo analítico Max Black en su libro "Critical Thinking" (Pensamiento Crítico) (1946). Fue posteriormente analizado por Solomon W. Golomb (1954), Gamow y Stern (1958) y por Martin Gardner en su columna del Scientific American "Juegos matemáticos". El problema se plantea como sigue:

Supóngase que a un tablero de ajedrez estándar de 8×8 se le eliminan dos esquinas diagonalmente opuestas, dejando 62 casillas. ¿Es posible colocar 31 piezas de dominó de tamaño 2×1 recubriendo todo el tablero?

La mayoría de las consideraciones sobre este problema en la literatura relacionada proporcionan soluciones "en el sentido conceptual", pero sin pruebas.^[1]​ John McCarthy lo propuso como un "problema duro" para sistemas de prueba automatizada.^[2]​ De hecho, la solución que utiliza el sistema de resolución por inferencia es exponencialmente duro.^[3]​

1. ↑ Andrews, Peter B.; Bishop, Matthew (1996), «On Sets, Types, Fixed Points, and Checkerboards», Theorem Proving With Analytic Tableaux and Related Methods: 5th International Workshop, Tableaux '96, Terrasini, Palermo, Italy, 15-17th, 1996, Proceedings, Lecture Notes in Computer Science, Springer-Verlag, «most treatments of the problem in the literature solve it in the conceptual sense, but do not actually provide proofs of the theorem in either of McCarthy's original formulations.» .
2. ↑ Arthan, R. D. (2005), The Mutilated Chessboard Theorem in Z (PDF), consultado el 6 de mayo de 2007, «The mutilated chessboard theorem was proposed over 40 years ago by John McCarthy as a “tough nut to crack” for automated reasoning.» .
3. ↑ Alekhnovich, Michael (2004), «Mutilated chessboard problem is exponentially hard for resolution», Theoretical Computer Science 310 (1-3): 513-525, doi:10.1016/S0304-3975(03)00395-5 ..